/*
 * $Id: DFSRTraverser.java 1259 2007-01-09 14:23:47Z tcoupaye $
 *
 * Behavior Protocols extensions for static and runtime checking
 * developed for the Julia implementation of Fractal.
 *
 * Copyright 2004
 *    Distributed Systems Research Group
 *    Department of Software Engineering
 *    Faculty of Mathematics and Physics
 *    Charles University, Prague
 *
 * Copyright (C) 2006
 *    Formal Methods In Software Engineering Group
 *    Institute of Computer Science
 *    Academy of Sciences of the Czech Republic
 *
 * Copyright (C) 2006 France Telecom
 *
 * This library is free software; you can redistribute it and/or
 * modify it under the terms of the GNU Lesser General Public
 * License as published by the Free Software Foundation; either
 * version 2 of the License, or (at your option) any later version.
 *
 * This library is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
 * Lesser General Public License for more details.
 *
 * You should have received a copy of the GNU Lesser General Public
 * License along with this library; if not, write to the Free Software
 * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307 USA
 *
 * Contact: ft@nenya.ms.mff.cuni.cz
 * Authors: Jan Kofron <kofron@nenya.ms.mff.cuni.cz>
 */

package org.objectweb.fractal.bpc.checker.DFSR;

import java.util.Stack;
import java.util.Iterator;

import org.objectweb.fractal.bpc.checker.node.*;
import org.objectweb.fractal.bpc.checker.parser.Debug;
import org.objectweb.fractal.bpc.checker.state.*;


/**
 * DFSR traverser performs the traversing of the graph generated by the given parse tree. 
 * It uses the DFS with Replacement algorithm.
 */
public class DFSRTraverser {

    /**
     * Creates a new instance of DFSRTraverser.
     * 
     * @param node the root of the parse tree
     * @param repository the action repository for printing the action names.
     */
    public DFSRTraverser(TreeNode node, ActionRepository repository) {
        this.node = node;

        if ((Options.action == Options.ACTIONTESTCOMPLIANCE) || (Options.action == Options.ACTIONTESTCONSENT)) { 
            //heuristics - a signature takes approximatelly 100B of memory
                this.globalCache = new StateCache(Options.statememory * (100000 / Signature.getSize()));
        } else
            this.globalCache = new StateCache(0);

        this.pathCache = new StateCache(0);
        this.pathStack = new Stack();
        this.repository = repository;
        this.secondStage = false;
    }

    /**
     * Performs the traversing through the graph and calling the appropriate methods of the given backend.
     * 
     * @param implementation the backend (either consent or visualization.
     * 
     * @throws CheckingException in the case a composition error is found
     */
    public void run(IDFSRExtension implementation) throws InvalidParameterException, ItemAlreadyPresentException, ItemNotPresentException, CheckingException {
        Stack poppedstack = new Stack();
        long statecnt = 1;
        State newstate;
        // initialization of the traversing
        newstate = node.getInitial();
        TransitionPair[] inittrans = null;
        boolean popflag = false;
        /*
        try {
            inittrans = node.getTransitions(initstate);
        } catch (CheckingException e) { // an accepting state found while
                                        // checking compliance
            throw e.addMessage("<initial state>");
        }
        */

        pathStack.push(new DFSRPathItem(-1, inittrans, newstate));
        pathCache.insert(newstate.getSignature());
        globalCache.insert(newstate.getSignature());
        //Debug.println(2, "state signature: " + initstate.getSignature());

        // action for the first state
        implementation.action(newstate);

        try {
            implementation.actionNew(newstate);
        } catch (AcceptingStateException e) {
            throw new AcceptingStateException("<initial state>");
        }
        
        Debug.print(3, "(S0) ");

        // main cycle of the traversing
        try {

	        while (pathStack.size() > 0) {
	            DFSRPathItem currentstatetuple = (DFSRPathItem) pathStack.peek();
	            //Debug.println("state: " + statecnt++);
	            
	            TransitionPair[] transitions = node.getTransitions(currentstatetuple.state).transitions;
	
	            // initialize the count of possible transitions
	            if (currentstatetuple.stateIndex == -1) 
	                currentstatetuple.stateIndex = transitions.length;
	                
	            if (popflag && (currentstatetuple.stateIndex < transitions.length)) {
	                Debug.println(3, repository.getItemString(transitions[currentstatetuple.stateIndex].eventIndex) + " ");
	                popflag = false;
	            }
	
	            // we decrease the index of active transition
	            if (currentstatetuple.stateIndex > 0) {
	                currentstatetuple.stateIndex--;
	
	                newstate = transitions[currentstatetuple.stateIndex].state;
	                
	                Debug.print(3, repository.getItemString(transitions[currentstatetuple.stateIndex].eventIndex) + " ");
	                Debug.print(3, "\n(S" + statecnt + ") ");
	                if ((statecnt & 1023) == 0) {
	                    Debug.println(2, Long.toString(statecnt));
	                    Debug.println(2, "Stack size:" + pathStack.size());
	                }
	
	                // we've found a cycle
	                if (pathCache.isPresent(newstate.getSignature())) {
	                    Debug.print(3, "cycle - staying current - ");
	                    implementation.action(newstate);
	                    if (Options.infiniteactivity != Options.IANO) {
	                        
		                    Iterator it = pathStack.iterator();
		                    Signature sig = newstate.getSignature();
		                    State stackstate = null;
		                    int stateindex = 0;
		                    while (it.hasNext()) {
		                        stackstate = ((DFSRPathItem) it.next()).state;
		                        if (sig.equals(stackstate.getSignature()))
		                            break;
		                        ++stateindex;
		                    }
		                    
		                    Debug.println(3, stackstate.label);
		                    
		                    if ((Options.infiniteactivity == Options.IAYES) && secondStage) {
			                    completeStack(pathStack,stateindex);
			                    ((DFSRPathItem)pathStack.peek()).transitions = node.getTransitions(((DFSRPathItem)pathStack.peek()).state).transitions;
			
			                    stackstate.cycleTrace = getStack(repository, pathStack, stateindex) + "(" + stackstate.label + ")";
		                    }
		                    
		                    implementation.actionCycle(stackstate);
		                    
		                    long oldid = currentstatetuple.state.getSignature().getCycleId();
		                    long newid = stackstate.getSignature().getCycleId();
		                    
		                    if ((oldid == Long.MAX_VALUE) || (oldid > newid)) {
		                        currentstatetuple.state.getSignature().setCycleId(newid);
		                        currentstatetuple.state.cycleStart = false;
		                        globalCache.updateItem(currentstatetuple.state.getSignature());
		                    }
		                    
		                    if (stateindex == pathStack.size())
		                        stackstate.cycleStart = false;
		                    
		                    if (!currentstatetuple.state.isAcceptingReachable() && (Options.infiniteactivity != Options.IANO)) {
		                        if (globalCache.acceptingReach(newstate.getSignature())) {
		                            currentstatetuple.state.getSignature().setAcceptingReachable(true);
		                            globalCache.setAcceptingReach(currentstatetuple.state.getSignature());
		                        }
		                    }
		                    
		                        
	                    }
	
	                }
	
	                // an already visited node is visiting again
	                else if (globalCache.isPresent(newstate.getSignature())) {
	                    Debug.print(3, "back - ");
	                    Debug.print(3, newstate.getSignature().toString());
	                    implementation.action(newstate);
	                    implementation.actionVisited(newstate);
	                    if (Options.infiniteactivity != Options.IANO) {
		                    if (!currentstatetuple.state.isAcceptingReachable() && (Options.infiniteactivity != Options.IANO)) {
		                        if (globalCache.acceptingReach(newstate.getSignature())) {
		                            currentstatetuple.state.getSignature().setAcceptingReachable(true);
		                            globalCache.setAcceptingReach(currentstatetuple.state.getSignature());
		                            Debug.print(3, " accepting - ");
		                        }
		                    }
		                    
		                    long oldid = currentstatetuple.state.getSignature().getCycleId();
		                    long newid = globalCache.getCycleId(newstate.getSignature());
		                    
		                    if ((oldid == Long.MAX_VALUE) || (oldid > newid)) {
		                        currentstatetuple.state.getSignature().setCycleId(newid);
		                        currentstatetuple.state.cycleStart = false;
		                        globalCache.updateItem(currentstatetuple.state.getSignature());
		                    }
	                    }
	                    Debug.println(3);
	                }
	
	                // a new node found (or a node removed from the global cache
	                // because of the memory amount used)
	                else {
	                    statecnt++;
	                    Debug.print(3, newstate.getSignature().toString());
	                    implementation.action(newstate);
	
	                        boolean isAccepting = false;
	                        if (implementation.actionNew(newstate)) {
	                            newstate.getSignature().setAcceptingReachable(true);
	                            isAccepting = true;
	                            Debug.print(3, "accepting - ");
	                        }
	
	
	                        // creating the new stackitem
	                        //TransitionPair[] newtrans = node.getTransitions(newstate);
	
	                        DFSRPathItem newitem = new DFSRPathItem(-1, null, newstate);
	                        pathStack.push(newitem);
	                        //newstate.createSignature();
	                        pathCache.insert(newstate.getSignature());
	                        globalCache.insert(newstate.getSignature());
	                        if ((Options.infiniteactivity != Options.IANO) && isAccepting)
	                            globalCache.updateItem(newstate.getSignature());
	
	                }
	            }
	
	            // all path from current node were explored
	            else {
	                popflag = true;
	                State current = currentstatetuple.state;
	                implementation.actionBack(current);
	
	                pathStack.pop();
	
	                if (pathStack.size() > 0) {
	                    
	                    if (Options.infiniteactivity != Options.IANO) {
		                    State above = ((DFSRPathItem) pathStack.peek()).state;
		                    
		                    Debug.print(3, current.isAcceptingReachable() ? "pop: accepting - " : "pop:not accepting - ");
		                    Debug.print(3, current.label + " " + current.getSignature().toString() + " - ");
		                    /*
		                    if (transitions.length > 0)
		                        Debug.println(3, repository.getItemString(transitions[0].eventIndex));
		                    */
		
		                    if (current.cycleStart && Options.action != Options.ACTIONVISUALIZE) {
		                        if (!current.isAcceptingReachable()) {
		                             if (!secondStage && Options.infiniteactivity == Options.IAYES) {
		                                popflag = false;
		                                Debug.println(2, "Infinite activity detected, reconstructing cycle trace");
		                                Debug.println(3, "Stack size: " + pathStack.size());
		                                Stack tmp = (Stack)pathStack.clone();
		                                completeStack(tmp, 0);
			                            ((DFSRPathItem)tmp.peek()).transitions = node.getTransitions(((DFSRPathItem)tmp.peek()).state).transitions;
		                                
		                                System.out.print("Prefix: " + getStack(repository, shortenStack(tmp), 0));
		                                
		                                secondStage = true;
		                                currentstatetuple.stateIndex = -1;
		                                pathStack.push(currentstatetuple);
		                                globalCache.clear();
		                                pathCache.clear();
		                                implementation.reset();
		                                
		                                for (int i = 0; i < pathStack.size(); ++i) {
		                                    Signature sig = ((DFSRPathItem)pathStack.get(i)).state.getSignature();
		                                    globalCache.insert(sig);
		                                    pathCache.insert(sig);
		                                    implementation.actionNew(((DFSRPathItem)pathStack.get(i)).state);
		                                }
		                                
		                            }
		                            else 
		                            {
			                            node.getAnotatedProtocol(current).prettyPrint(true);
			                            completeStack(pathStack, 0);
			                            
			                            ((DFSRPathItem)pathStack.peek()).transitions = node.getTransitions(((DFSRPathItem)pathStack.peek()).state).transitions;
			                            
			                            System.out.println('(' + current.label + ')' + "\nCycle: " + (Options.infiniteactivity == Options.IAYES ? current.cycleTrace : "cycle trace no available, run with --infiniteactivity=yes"));
			                            throw new InfiniteActivityException("divergence.");
		                            }
		                        }
		                    } else {
		                        long aboveid = above.getSignature().getCycleId();
		                        long currentid = current.getSignature().getCycleId();
		                        if (((aboveid == Long.MAX_VALUE) || (aboveid > currentid)) && (currentid != Long.MAX_VALUE)) {
		                            above.getSignature().setCycleId(currentid);
		                            above.cycleStart = false;
		                            poppedstack.push(currentstatetuple);
		                        }
		                    }
		                    
		                    if (!above.isAcceptingReachable() && current.isAcceptingReachable()) {
		                            above.getSignature().setAcceptingReachable(true);
		                            globalCache.updateItem(above.getSignature());
		                    }
	                    }
	                }
	
	                if (popflag)
	                    pathCache.remove(currentstatetuple.state.getSignature());
	                // the node should stay in the global cache for now
	                
	                popflag = true;
	            }
	            
	
	        }
            Debug.println(statecnt + " states visited.");

        }
        catch (InfiniteActivityException e) {
			Debug.println(statecnt + " states visited (some of them are counted more than once).");
			node.getAnotatedProtocol(newstate).prettyPrint(true);
			throw e;
        } 
        catch (CheckingException e) { // an accepting state found while checking compliance
			//pathStack.push(new DFSRPathItem(0, new TransitionPair[0], newstate));
			Debug.println(statecnt + " states visited.");
			node.getAnotatedProtocol(newstate).prettyPrint(true);
			
			completeStack(pathStack, 0);
			
			throw e.addMessage(getStack(repository, shortenStack(pathStack), 0));
		}

    }

    /**
     * @return the action sequence stored at the stack
     */
    static String getStack(ActionRepository repository, Stack stack, int from) {
        String result = new String("\n");
        
        if (stack.size() == 1)
            return ("<initial state>");
        else {

	        for (int i = from; i < stack.size(); ++i) {
	            DFSRPathItem item = (DFSRPathItem) stack.get(i);
	            result += "(" + item.state.label + ")";
	            if ((item.stateIndex >= 0) && (item.transitions.length > 0) && (item.stateIndex < item.transitions.length)) {
                    String event = repository.getItemString(item.transitions[item.stateIndex].eventIndex);
                    if ((event.charAt(0) != '[') && (event.indexOf('<') != -1)) {
                        String method = event.substring(event.indexOf('.') + 1, event.length());
                        String iface = event.substring(event.indexOf('-') + 1, event.indexOf('>'));
                        result += " " + event.charAt(0) + iface + "." + method + " \n";
                    }
                    else // atomic action or unstructured iface
                        result += " " + event + " \n";
                    
	                
                }
	        }
	
	        return result;
        }
    }

    /**
     * Optimizes the stack listing by omitting those transitions that are not
     * necessary (omitting "cycles")
     * 
     * @return eventually shortened trace
     */
    private Stack shortenStack(Stack stack) {
        // the main cycle from the stack top to the bottom
        int i = stack.size() - 1;
        while (i > 0) {
            State higherstate = ((DFSRPathItem) stack.get(i)).state;
            int j = 0;
            while (j < i - 1) {
                DFSRPathItem lower = (DFSRPathItem) stack.get(j);
                int transcnt = lower.transitions.length;
                for (int k = 0; k < transcnt; ++k) {
                    if (lower.transitions[k].state.equals(higherstate)) { // we
                                                                          // found
                                                                          // a
                                                                          // "cycle"
                        for (int l = i - 1; l > j; --l) {
                            stack.removeElementAt(l);
                        }

                        lower.stateIndex = k;
                        i = j;
                        j = -1;
                        break;
                    }
                }
                ++j;
            }
            --i;
        }

        return stack;
    }
    
    /**
     * Regenerates all transitions for state at stack.
     * @param stack the stack
     */
    private void completeStack(Stack stack, int stateindex) {
        for (int i = stateindex; i < stack.size() - 1; ++i) {
            DFSRPathItem item = (DFSRPathItem)stack.get(i);
            try {
                item.transitions = node.getTransitions(item.state).transitions;
            }
            catch (CheckingException e) {
                System.out.println("Internal checker error");
            }
            catch (InvalidParameterException e) {
                System.out.println("Internal checker error");
            }
        }
    }

    /**
     * Initial node of the traversing
     */
    private TreeNode node;

    /**
     * The cache for storing already globally visited states.
     */
    private StateCache globalCache;

    /**
     * The cache for the stack of actual traversal path for fast lookup.
     */
    private StateCache pathCache;

    /**
     * The stack for storing the actual path.
     */
    private Stack pathStack;

    /**
     * Action repository
     */
    private ActionRepository repository;
    
    /**
     * Flag for denoting the stage phase when reporting the infinite activity
     */
    private boolean secondStage;

}
